;; TO JEST TYLKO WERSJA ROBOCZA, NIE SPRAWDZANA KOMPUTEROWO
;; MOŻE ZAWIERAĆ BŁĘDY


(set xd-1a
     (Pi (A (Universe 0)) (a A)
         (alfa (Id (refl a) (refl a)))
         (beta (Id (refl a) (refl a)))
         (Id
          ;; alfa o  beta
          (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
          ;; alfa gwiazdka beta
          (horizontal-composition A a a a
                                  (refl a) (refl a) (refl a) (refl a)
                                  alfa beta)))
     (lambda (A (Universe 0)) (a A)
       (alfa (Id (refl a) (refl a)))
       (beta (Id (refl a) (refl a)))
       (refl (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)))) ;; (refl to-drugie) też by było

(set xd-2a
     (Pi (A (Universe 0)) (a A)
         (alfa (Id (refl a) (refl a)))
         (beta (Id (refl a) (refl a)))
         (Id
          ;; alfa gwiazdka' beta
          (horizontal-composition-2 A a a a
                                  (refl a) (refl a) (refl a) (refl a)
                                  alfa beta)
          ;; beta o  alfa
          (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)
))
     (lambda (A (Universe 0)) (a A)
       (alfa (Id (refl a) (refl a)))
       (beta (Id (refl a) (refl a)))
       (refl (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)))) ;; (refl to-drugie) też by było

(set hc-eq-hc2
     (Pi (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b))
         (r (Id b c)) (s (Id b c))
         (alfa (Id p q)) (beta (Id r s))
         (horizontal-composition A a b c p q r s alfa beta)
         (horizontal-composition-2 A a b c p q r s alfa beta))
     (lambda
       (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b))
         (r (Id b c)) (s (Id b c))
         (alfa (Id p q)) (beta (Id r s))
     ;;TODO 4xJ (alfa, beta, p ,r) +   (refl (refl a))
         ))


(set eh
     (Pi (A (Universe 0)) (a A)
         (alfa (Id (refl a) (refl a)))
         (beta (Id (refl a) (refl a)))
         (Id ;KOZACKIE TWIERDZENIE :DDDDD
          (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
          (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)))
     (lambda (A (Universe 0)) (a A)
       (alfa (Id (refl a) (refl a)))
       (beta (Id (refl a) (refl a)))
       (concat
        (Id (refl a) (refl a))
        (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
        (horizontal-composition-2 A a a a (refl a) (refl a) (refl a) (refl a) alfa beta)
        (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)
        (concat (Id (refl a) (refl a))
                (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
                (horizontal-composition A a a a (refl a) (refl a) (refl a) (refl a) alfa beta)
                (horizontal-composition-2 A a a a (refl a) (refl a) (refl a) (refl a) alfa beta)
                (xd-1a A a alfa beta)
                (hc-eq-hc2 A a a a (refl a) (refl a) (refl a) (refl a) alfa beta))
        (xd-2a A a alfa beta))))
